#include "formule.hpp"
#include "sat.hpp"
#include "parser.hpp"
#include <iostream>
#include <fstream>
#include <cstdlib>

using namespace std;

int main(int argc, char** argv) {
  formule f;
  if (argc <= 1)
    f = lit_formule(cin);
  else
    f = lit_formule(string(argv[1]));

  cnf_t retour = tseitin(f);

  vector<val_t> valeurs;

  for(unsigned int i = 0; i < retour.size(); i++)
  {
	  valeurs.push_back(INDETERMINEE);
  }

  cout << cherche(valeurs, 0, retour) << endl;
    
  cout << f << endl;
  free_all(f);
  return EXIT_SUCCESS;
}
